p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p)) 

latex

Definitions	atomic(a), P  Q, b | a, P & Q, prime(a), x:A. B(x), t  T, reducible(a), x. t(x), P  Q, P  Q, x:A. B(x), P  Q, Prop, , a  b, False, Dec(P), a ~ b, A, T, True
Lemmas	assoced inversion, true wf, squash wf, multiply functionality wrt assoced, assoced functionality wrt assoced, assoced weakening, nequal wf, decidable int equal, not wf, decidable assoced, decidable not, assoced wf, int nzero wf, dneg elim a, or functionality wrt iff, not over and, iff transitivity, all functionality wrt iff, not over exists, prime wf, divides wf, prime imp atomic